var jseval = {} ;

jseval.allocAval =
  function (address, value, stack, store, c)
  {
    var store2 = store.allocAval(address, value);
    return store2;
  }

jseval.lookupAval =
  function (address, stack, store, c)
  {
    var result = store.lookupAval(address);
//    print("LOOKUP", address, result);
    return result;
  }

jseval.updateAval =
  function (address, value, stack, store, c)
  {
    var store2 = store.updateAval(address, value);
//    print("UPDATE", address, value);
    return store2;
  }

jseval.sideEffectAval =
  function (address, value, stack, store, c)
  {
    var store2 = store.updateAval(address, value);
//    print("SIDE", address, value);
    return store2;
  }

jseval.doLookupAddresses =
  function (addresses, stack, store, c)
  {
    var result = BOT;
    addresses.forEach(
      function (address)
      {
        var aval = c.e.lookupAval(address, stack, store, c);
        result = result.join(aval);
      });
    return result;
  } 

jseval.doScopeLookup =
  function (name, stack, benva, store, c)
  {
    var result = BOT;
    var benvas = [benva];
    while (benvas.length !== 0)
    {
      var a = benvas[0];
      benvas = benvas.slice(1);
      var benv = c.e.lookupAval(a, stack, store, c);
      var lookup = benv.lookup(name);
      result = result.join(lookup.value);
      if (lookup.value !== BOT)
//        if (lookup.directMatch)
      {
        return result;
      }
      benvas = benvas.concat(benv.parents);
    }
    // TODO: should we split on 'directMatch' into two states (found/not found)?
//    if (!lookup.directMatch && result === BOT)
//    {
      throw new Error("ReferenceError: " + name + " is not defined"); //TODO turn this into stack trace
//    }
//    return result;
  }

jseval.doScopeSet =
  function (name, value, stack, benva, store, c)
  {
    var result = BOT;
    var benvas = [benva];
    while (benvas.length !== 0)
    {
      var a = benvas[0];
      benvas = benvas.slice(1);
      var benv = c.e.lookupAval(a, stack, store, c);
      var lookup = benv.lookup(name);
      if (lookup.value !== BOT)
      {
        benv = benv.add(name, value);
        store = c.e.sideEffectAval(a, benv, stack, store, c);
      }
      if (lookup.value !== BOT)
//        if (lookup.directMatch)
      {
        break;
      }
      benvas = benvas.concat(benv.parents);
    }
    return store;
  }

jseval.doProtoLookup =
  function (object, propertyName, stack, store, c)
  {
    var objects = [object];
    var result = BOT;
    while (objects.length > 0)
    {
      var object = objects[0];
      objects = objects.slice(1);
//      print("protoLookup", propertyName, "in", object.names(), "for", object);
      var lookup = object.lookup(propertyName);
      result = result.join(lookup.value);
      if (lookup.value === BOT)
//        if (lookup.directMatch)
      {
        // TODO proper coercions?
        if (object.Prototype.user.subsumes(c.l.U_NULL))
        {
           result = result.join(c.l.J_UNDEFINED);
        }
        var cprotoAddresses = object.Prototype.addresses();
        if (!cprotoAddresses)
        {
          throw new Error("doProtoLookup: no addresses for " + object.Prototype);
          //return fcont(null); // TODO null checks are still in place everywhere this function is called
        }
        cprotoAddresses.forEach(
          function (protoAddress)
          {
            var protoObject = c.e.lookupAval(protoAddress, stack, store, c);
            objects = objects.addLast(protoObject);         
          });
      }
    }
    return result;
  }
  
jseval.evalLiteral =
  function (node, stack, benva, store, time, c)
  {
    var cont = stack[0];
    var stack2 = stack.slice(1);
    return cont.execute(stack2.addFirst(c.l.abst1(node.value)), store, time, c);
  }

jseval.evalIdentifier =
  function (node, stack, benva, store, time, c)
  {
    var cont = stack[0];
    var stack2 = stack.slice(1);
    var value = c.e.doScopeLookup(c.l.userLattice.abst1(node.name), stack, benva, store, c);
    return cont.execute(stack2.addFirst(value), store, time, c);
  }

jseval.evalBinaryExpression =
  function (node, stack, benva, store, time, c)
  {
    var leftNode = node.left;
    var rightNode = node.right;
  
    function leftCont()
    {
      function rightCont()
      {
        
        function mul(stack, store, time, c)
        {
          var right = stack[0];
          var left = stack[1];
          var cont = stack[2];
          var stack2 = stack.slice(3);
          var result = c.l.userLattice.mul(left.user, right.user);
          return cont.execute(stack2.addFirst(new JipdaValue(result, [])), store, time, c);
        }
        function sub(stack, store, time, c)
        {
          var right = stack[0];
          var left = stack[1];
          var cont = stack[2];
          var stack2 = stack.slice(3);
          var result = c.l.userLattice.sub(left.user, right.user);
          return cont.execute(stack2.addFirst(new JipdaValue(result, [])), store, time, c);
        }
        function div(stack, store, time, c)
        {
          var right = stack[0];
          var left = stack[1];
          var cont = stack[2];
          var stack2 = stack.slice(3);
          var result = c.l.userLattice.div(left.user, right.user);
          return cont.execute(stack2.addFirst(new JipdaValue(result, [])), store, time, c);
        }
        function rem(stack, store, time, c)
        {
          var right = stack[0];
          var left = stack[1];
          var cont = stack[2];
          var stack2 = stack.slice(3);
          var result = c.l.userLattice.rem(left.user, right.user);
          return cont.execute(stack2.addFirst(new JipdaValue(result, [])), store, time, c);
        }
        function lt(stack, store, time, c)
        {
          var right = stack[0];
          var left = stack[1];
          var cont = stack[2];
          var stack2 = stack.slice(3);
          var result = c.l.userLattice.lt(left.user, right.user);
          return cont.execute(stack2.addFirst(new JipdaValue(result, [])), store, time, c);
        }
        function lte(stack, store, time, c)
        {
          var right = stack[0];
          var left = stack[1];
          var cont = stack[2];
          var stack2 = stack.slice(3);
          var result = c.l.userLattice.lte(left.user, right.user);
          return cont.execute(stack2.addFirst(new JipdaValue(result, [])), store, time, c);
        }
        function gt(stack, store, time, c)
        {
          var right = stack[0];
          var left = stack[1];
          var cont = stack[2];
          var stack2 = stack.slice(3);
          var result = c.l.userLattice.gt(left.user, right.user);
          return cont.execute(stack2.addFirst(new JipdaValue(result, [])), store, time, c);
        }
        function gte(stack, store, time, c)
        {
          var right = stack[0];
          var left = stack[1];
          var cont = stack[2];
          var stack2 = stack.slice(3);
          var result = c.l.userLattice.gte(left.user, right.user);
          return cont.execute(stack2.addFirst(new JipdaValue(result, [])), store, time, c);
        }
        
        // 11.9.3
        function eq(eqFlag, stack, store, time, c)
        {
          var rightAval = stack[0];
          var leftAval = stack[1];
          var eqResult = BOT; // primitive value
          var lasl = leftAval.as.length;
          var rasl = rightAval.as.length;
          
          if (leftAval.user !== BOT && rightAval.user !== BOT)
          {
            eqResult = eqResult.join(eqFlag ? c.l.userLattice.eq(leftAval.user, rightAval.user) : c.l.userLattice.neq(leftAval.user, rightAval.user));
          }
          
          // only primitives: done (shortcut)
          if (lasl === 0 && rasl === 0)
          {
            var cont = stack[2];
            var stack2 = stack.slice(3);
            return cont.execute(stack2.addFirst(new JipdaValue(eqResult, [])), store, time, c);                                      
          }
          else if (lasl === 1 && rasl === 1)
          {
            if (leftAval.as[0].equals(rightAval.as[0]))
            {
              eqResult = eqResult.join(eqFlag ? c.l.U_TRUE : c.l.U_FALSE);
            }
            else
            {
              eqResult = eqResult.join(eqFlag ? c.l.U_FALSE : c.l.U_TRUE);
            }
          }
          else if (lasl > 0 && rasl > 0)
          {
            eqResult = eqResult.join(eqFlag ? c.l.U_FALSE : c.l.U_TRUE);
            var intersection = leftAval.as.keepAll(rightAval.as);
            if (intersection.length > 0)
            {
              eqResult = eqResult.join(eqFlag ? c.l.U_TRUE : c.l.U_FALSE);
            }
          }
          
          // only addresses: done (shortcut)
          if (leftAval.user === BOT && rightAval.user === BOT)
          {
            var cont = stack[2];
            var stack2 = stack.slice(3);
            return cont.execute(stack2.addFirst(new JipdaValue(eqResult, [])), store, time, c);                                                        
          }
          
          function eqLeftRightCont(leftStrNum, eqResult)
          {
            return new Cont("eqLeftRight", node, null, benva,
              function (stack, store, time, c)
              {
                var rightPrim = stack[0];
                // [1] [2] rightAval leftAval
                var cont = stack[3];
                var stack2 = stack.slice(4);
                eqResult = eqResult.join(eqFlag ? c.l.userLattice.eq(leftStrNum, rightPrim.user) : c.l.userLattice.neq(leftStrNum, rightPrim.user));
                return cont.execute(stack2.addFirst(new JipdaValue(eqResult, [])), store, time, c);                                      
              });
          }                
          
          if (leftAval.as.length !== 0)
          {
            function eqRightCont(rightStrNum, eqResult)
            {
              return new Cont("eqRight", rightNode, null, benva,
                function (stack, store, time, c)
                {                      
                  var leftPrim = stack[0];
                  eqResult = eqResult.join(eqFlag ? c.l.userLattice.eq(leftPrim.user, rightStrNum) : c.l.userLattice.neq(leftPrim.user, rightStrNum));
                  // start clone
                  if (rightAval.as.length !== 0) 
                  {
                    var leftStrNum = leftAval.user.projectStringNumber();
                    if (leftStrNum !== BOT)
                    {
                      var isOnlyStrNum = (leftStrNum.equals(leftAval.user));
                      if (!isOnlyStrNum)
                      {
                        eqResult = eqResult.join(eqFlag ? c.l.U_FALSE : c.l.U_TRUE);
                      }
                      var stack2 = stack.slice(1);
                      return c.e.DefaultValue(rightAval.as, undefined, rightNode, stack2.addFirst(eqLeftRightCont(eqResult, leftStrNum)), benv, store, time, c);                      
                    }
                    else
                    {
                      eqResult = eqResult.join(eqFlag ? c.l.U_FALSE : c.l.U_TRUE);
                    }
                  }
                  // end clone
                  
                  // [1] [2] rightAval leftAval
                  var cont = stack[3];
                  var stack2 = stack.slice(4);
                  return cont.execute(stack2.addFirst(new JipdaValue(eqResult, [])), store, time, c);                        
                });
            }
            
            var rightStrNum = rightAval.user.projectStringNumber();
            if (rightStrNum !== BOT)
            {
              var isOnlyStrNum = (rightStrNum.equals(rightAval.user));
              if (!isOnlyStrNum)
              {
                eqResult = eqResult.join(eqFlag ? c.l.U_FALSE : c.l.U_TRUE);
              }
              return c.e.DefaultValue(leftAval.as, undefined, leftNode, stack.addFirst(eqRightCont(rightStrNum, eqResult)), benva, store, time, c);                      
            }
            else
            {
              eqResult = eqResult.join(eqFlag ? c.l.U_FALSE : c.l.U_TRUE);
            }
          }
          if (rightAval.as.length !== 0) 
          {
            var leftStrNum = leftAval.user.projectStringNumber();
            if (leftStrNum !== BOT)
            {
              var isOnlyStrNum = (leftStrNum.equals(leftAval.user));
              if (!isOnlyStrNum)
              {
                eqResult = eqResult.join(eqFlag ? c.l.U_FALSE : c.l.U_TRUE);
              }
              return c.e.DefaultValue(rightAval.as, undefined, rightNode, stack.addFirst(eqLeftRightCont(leftStrNum, eqResult)), benva, store, time, c);                      
            }
            else
            {
              eqResult = eqResult.join(eqFlag ? c.l.U_FALSE : c.l.U_TRUE);
            }
          }
          var cont = stack[2];
          var stack2 = stack.slice(3);
          return cont.execute(stack2.addFirst(new JipdaValue(eqResult, [])), store, time, c);                                      
        }
  
        
        return new Cont("binr", rightNode, null, benva,
          function (stack, store, time, c)
          {
            var rightAval = stack[0];
            var leftAval = stack[1];
                        
            switch (node.operator)
            {
              case "+":
              {
                var rightAval = stack[0];
                var leftAval = stack[1];
                var result = BOT; // primitive value
                var lasl = leftAval.as.length;
                var rasl = rightAval.as.length;
                
                if (leftAval.user !== BOT && rightAval.user !== BOT)
                {
                  result = result.join(c.l.userLattice.add(leftAval.user, rightAval.user));
                }
                
                if (lasl === 0 && rasl === 0)
                {
                  var cont = stack[2];
                  var stack2 = stack.slice(3);
                  return cont.execute(stack2.addFirst(new JipdaValue(result, [])), store, time, c);                  
                }
                
                if (lasl > 0)
                {
                  function addLeftCont(result)
                  {
                    return new Cont("addl", leftNode, null, benva,
                      function (stack, store, time, c)
                      {
                        var lprim = stack[0].user;
  
                        if (rightAval.user !== BOT)
                        {
                          result = result.join(c.l.userLattice.add(lprim, rightAval.user));
                        }
                        if (rasl > 0)
                        {
                          function addLeftRightCont(result)
                          {
                            return new Cont("addlr", rightNode, null, benva,
                              function (stack, store, time, c)
                              {
                                var rprim = stack[0].user;
                                if (leftAval.user !== BOT)
                                {
                                  result = result.join(c.l.userLattice.add(leftAval.user, rprim));
                                }
                                result = result.join(c.l.userLattice.add(lprim, rprim));
                                var cont = stack[4];
                                var stack2 = stack.slice(5);
                                return cont.execute(stack2.addFirst(new JipdaValue(result, [])), store, time, c);                                                  
                              });
                          }
                          return c.e.DefaultValue(rightAval.as, undefined, leftNode, stack.addFirst(addLeftRightCont(result)), benva, store, time, c);                          
                        }
                        var cont = stack[3];
                        var stack2 = stack.slice(4);
                        return cont.execute(stack2.addFirst(new JipdaValue(result, [])), store, time, c);                                                                          
                      });
                  }
                  
                  return c.e.DefaultValue(leftAval.as, undefined, leftNode, stack.addFirst(addLeftCont(result)), benva, store, time, c);
                }
                
                if (rasl > 0)
                {
                  function addRightCont(result)
                  {
                    return new Cont("addr", rightNode, null, benva,
                      function (stack, store, time, c)
                      {
                        var rprim = stack[0].user;
                        result = result.join(c.l.userLattice.add(leftAval.user, rprim)); // luser must be present when lasl == 0
                        var cont = stack[3];
                        var stack2 = stack.slice(4);
                        return cont.execute(stack2.addFirst(new JipdaValue(result, [])), store, time, c);                                                  
                      });
                  }
                  return c.e.DefaultValue(rightAval.as, undefined, leftNode, stack.addFirst(addRightCont(result)), benva, store, time, c);                          
                }
                
                var cont = stack[2];
                var stack2 = stack.slice(3);
                return cont.execute(stack2.addFirst(new JipdaValue(result, [])), store, time, c);                
              }
              case "*":
              {
                if (leftAval.as.length + rightAval.as.length === 0)
                {
                  return mul(stack, store, time, c);
                }
                throw new Error("TODO");
              }
              case "-":
              {
                if (leftAval.as.length + rightAval.as.length === 0)
                {
                  return sub(stack, store, time, c);
                }
                throw new Error("TODO");
              }
              case "/":
              {
                if (leftAval.as.length + rightAval.as.length === 0)
                {
                  return div(stack, store, time, c);
                }
                throw new Error("TODO");
              }
              case "%":
              {
                if (leftAval.as.length + rightAval.as.length === 0)
                {
                  return rem(stack, store, time, c);
                }
                throw new Error("TODO");
              }
              case "===":
              {
                var rightAval = stack[0];
                var leftAval = stack[1];
                var result = BOT; // primitive value
                var lasl = leftAval.as.length;
                var rasl = rightAval.as.length;
                
                if (leftAval.user !== BOT && rightAval.user !== BOT)
                {
                  result = result.join(c.l.userLattice.eqq(leftAval.user, rightAval.user));
                }
                
                if (lasl === 0 && rasl === 0)
                {
                  var cont = stack[2];
                  var stack2 = stack.slice(3);
                  return cont.execute(stack2.addFirst(new JipdaValue(result, [])), store, time, c);                  
                }
                
                if (lasl === 1 && rasl === 1)
                {
                  if (leftAval.as[0].equals(rightAval.as[0]))
                  {
                    result = result.join(c.l.U_TRUE);
                  }
                  else
                  {
                    result = result.join(c.l.U_FALSE);
                  }
                }
                else if (lasl > 0 && rasl > 0)
                {
                  result = result.join(c.l.U_FALSE);
                  if ((leftAval.as.intersect(rightAval.as)).length > 0)
                  {
                    result = result.join(c.l.U_TRUE);
                  }
                }
                
                if (leftAval.user === BOT && rightAval.user === BOT)
                {
                  var cont = stack[2];
                  var stack2 = stack.slice(3);
                  return cont.execute(stack2.addFirst(new JipdaValue(result, [])), store, time, c);                  
                }
                
                result = result.join(c.l.U_FALSE);
                var cont = stack[2];
                var stack2 = stack.slice(3);
                return cont.execute(stack2.addFirst(new JipdaValue(result, [])), store, time, c);                
              }
              case "!==":
              {
                var rightAval = stack[0];
                var leftAval = stack[1];
                var result = BOT; // primitive value
                var lasl = leftAval.as.length;
                var rasl = rightAval.as.length;
                
                if (leftAval.user !== BOT && rightAval.user !== BOT)
                {
                  result = result.join(c.l.userLattice.neqq(leftAval.user, rightAval.user));
                }
                
                if (lasl === 0 && rasl === 0)
                {
                  var cont = stack[2];
                  var stack2 = stack.slice(3);
                  return cont.execute(stack2.addFirst(new JipdaValue(result, [])), store, time, c);                  
                }
                
                if (lasl === 1 && rasl === 1)
                {
                  if (leftAval.as[0].equals(rightAval.as[0]))
                  {
                    result = result.join(c.l.U_FALSE);
                  }
                  else
                  {
                    result = result.join(c.l.U_TRUE);
                  }
                }
                else if (lasl > 0 && rasl > 0)
                {
                  result = result.join(c.l.U_TRUE);
                  if ((leftAval.as.intersect(rightAval.as)).length > 0)
                  {
                    result = result.join(c.l.U_FALSE);
                  }
                }
                
                if (leftAval.user === BOT && rightAval.user === BOT)
                {
                  var cont = stack[2];
                  var stack2 = stack.slice(3);
                  return cont.execute(stack2.addFirst(new JipdaValue(result, [])), store, time, c);                  
                }
                
                result = result.join(c.l.U_TRUE);
                var cont = stack[2];
                var stack2 = stack.slice(3);
                return cont.execute(stack2.addFirst(new JipdaValue(result, [])), store, time, c);                
  
              }
              case "==":
              {
                return eq(true, stack, store, time, c);
              }
              case "!=":
              {
                return eq(false, stack, store, time, c);
              }
              case "<":
              {
                if (leftAval.as.length + rightAval.as.length === 0)
                {
                  return lt(stack, store, time, c);
                }
                throw new Error("TODO");
                // reduce with number!
              }
              case "<=":
              {
                if (leftAval.as.length + rightAval.as.length === 0)
                {
                  return lte(stack, store, time, c);
                }
                throw new Error("TODO");
                // reduce with number!
              }
              case ">":
              {
                if (leftAval.as.length + rightAval.as.length === 0)
                {
                  return gt(stack, store, time, c);
                }
                throw new Error("TODO");
                // reduce with number!
              }
              case ">=":
              {
                if (leftAval.as.length + rightAval.as.length === 0)
                {
                  return gte(stack, store, time, c);
                }
                throw new Error("TODO");
                // reduce with number!
              }
              case "&":
              {
                var lu = toUserInt32(leftAval);
                var ru = toUserInt32(rightAval);
                var result = c.l.userLattice.binand(lu, ru);
                var cont = stack[2];
                var stack2 = stack.slice(3);
                return cont.execute(stack2.addFirst(new JipdaValue(result, [])), store, time, c);
              }
              case "|":
              {
                var lu = toUserInt32(leftAval);
                var ru = toUserInt32(rightAval);
                var result = c.l.userLattice.binor(lu, ru);
                var cont = stack[2];
                var stack2 = stack.slice(3);
                return cont.execute(stack2.addFirst(new JipdaValue(result, [])), store, time, c);
              }
              case "<<":
              {
                if (leftAval.as.length + rightAval.as.length === 0)
                {
                  var right = stack[0];
                  var left = stack[1];
                  var cont = stack[2];
                  var stack2 = stack.slice(3);
                  var result = c.l.userLattice.shl(left.user, right.user);
                  return cont.execute(stack2.addFirst(new JipdaValue(result, [])), store, time, c);
                }
                throw new Error("TODO");
              }              
              default: throw new Error("cannot handle binary operator " + node.operator);
            }            
          });
      }
      
      return new Cont("binl", leftNode, null, benva,
        function (stack, store, time, c)
        {
          return c.e.evalNode(rightNode, stack.addFirst(rightCont()), benva, store, time, c);
        });
    }
    
    return c.e.evalNode(leftNode, stack.addFirst(leftCont()), benva, store, time, c);
  }

jseval.evalProgram =
  function (node, stack, benva, store, time, c)
  {
    var hoisted = node.hoisted;
    if (!hoisted)
    {
      var scopeInfo = Ast.scopeInfo(node);
      hoisted = Ast.hoist(scopeInfo);
      node.hoisted = hoisted;
    }
    if (hoisted.funs.length > 0 || hoisted.vars.length > 0)
    {
      var benv = c.e.lookupAval(benva, stack, store, c);      
      hoisted.funs.forEach(
        function (funDecl)
        {
          var result = c.e.evalHoistedFunctionDeclaration(funDecl.node, stack, benva, benv, store, time, c);
          benv = result.benv;
          store = result.store;
        });
      hoisted.vars.forEach(
          function (varDecl)
          {
            var result = c.e.evalHoistedVariableDeclarator(varDecl.node, stack, benv, store, time, c);
            benv = result.benv;
            store = result.store;
          });
      store = c.e.sideEffectAval(benva, benv, stack, store, c);
    }
    
    var bodyNodes = node.body;
    return c.e.evalStatementList(bodyNodes, stack, benva, store, time, c);
  }

jseval.evalHoistedVariableDeclarator =
  function (node, stack, benv, store, time, c)
  { 
    var vr = node.id;    
//    var address = c.a.variable(vr, time);
//  benv = benv.add(c.l.userLattice.abst1(vr.name), c.l.J_UNINITIALIZED);
      benv = benv.add(c.l.userLattice.abst1(vr.name), c.l.J_UNDEFINED);
//    store = c.e.allocAval(address, BOT, stack, store, c);
    return {benv: benv, store: store};      
  } 

  // with last value on stack
jseval.evalStatementList =
  function (nodes, stack, benva, store, time, c)
  {
    function statementListCont(i)
    {
      return new Cont("slist", nodes[i - 1], null, benva,
        function (stack, store, time, c)
        {
          var statementValue = stack[0];
          var value = stack[1];
          
          // keep track of last value-producing statement (ECMA 12.1 Block, 14 Program)
          if (!statementValue.equals(c.l.J_UNDEFINED))
          {
            value = statementValue;
            var str = value.toString(); value.toString = function () {return str + "|"}; //DEBUG
          }
          
          if (i === nodes.length)
          {
            var cont = stack[2];
            var stack2 = stack.slice(3);
            return cont.execute(stack2.addFirst(value), store, time, c);
          }
          var stack2 = stack.slice(2);
          return c.e.evalNode(nodes[i], stack2.addFirst(value).addFirst(statementListCont(i + 1)), benva, store, time, c);
        });
    };
    
    if (nodes.length === 0)
    {
      var cont = stack[0];
      var stack2 = stack.slice(1);
      return cont.execute(stack2.addFirst(c.l.J_UNDEFINED), store, time, c);
    }
    if (nodes.length === 1)
    {
      return c.e.evalNode(nodes[0], stack, benva, store, time, c);
    }
    return c.e.evalNode(nodes[0], stack.addFirst(c.l.J_UNDEFINED).addFirst(statementListCont(1)), benva, store, time, c);
  }

jseval.evalVariableDeclarator =
  function (node, stack, benva, store, time, c)
  { 
    var vr = node.id;
    c.e.markNode(vr);
  
    function variableDeclaratorCont()
    {
      return new Cont("decl", node.init, null, benva,
        function (stack, store, time, c)
        {
          var value = stack[0];
          var cont = stack[1];
          var stack2 = stack.slice(2);
//          var as = c.e.doScopeLookup(c.l.userLattice.abst1(vr.name), stack, benva, store, c);
//          if (as.length === 0)
//          {
//            throw new Error("no addresses for " + node);
//          }
//          as.forEach(
//            function (address)
//            {
//              store = c.e.updateAval(address, value, stack, store, c);
//            });
          var benv = c.e.lookupAval(benva, stack, store, c);
          benv = benv.add(c.l.userLattice.abst1(vr.name), value);
          store = c.e.sideEffectAval(benva, benv, stack, store, c);
          return cont.execute(stack2.addFirst(c.l.J_UNDEFINED), store, time, c);
        });
    }
    
    if (node.init === null)
    {
      var cont = stack[0];
      var stack2 = stack.slice(1);
      return cont.execute(stack2.addFirst(c.l.J_UNDEFINED), store, time, c);      
    }
    return c.e.evalNode(node.init, stack.addFirst(variableDeclaratorCont()), benva, store, time, c);
  } 

jseval.evalObjectExpression =
  function(node, stack, benv, store, time, c)
  {
    var properties = node.properties;
    
    function objectCont(i)
    {
      return new Cont("obj", properties[i - 1].value, null, benv,
        function (stack, store, time, c)
        {
          if (i === properties.length)
          {
            var rexps = stack.slice(0, properties.length);
            var cont = stack[properties.length];
            var stack2 = stack.slice(properties.length + 1);
            var obj = c.createObject(c.OBJECTPA);
            var objectAddress = c.a.object(node, time);
            for (var k = properties.length - 1; k > -1; k--)
            {
              var propertyName = c.l.userLattice.abst1(properties[properties.length - k - 1].key.name);
              obj = obj.add(propertyName, rexps[k]);
            }
            store = c.e.allocAval(objectAddress, obj, stack, store, c);
            return cont.execute(stack2.addFirst(c.l.abst1(objectAddress)), store, time, c);
          }
          return c.e.evalNode(properties[i].value, stack.addFirst(objectCont(i + 1)), benv, store, time, c);
        });
    }
    
    if (properties.length === 0)
    { 
      var cont = stack[0];
      var stack2 = stack.slice(1);
      var obj = c.createObject(c.OBJECTPA);
      var objectAddress = c.a.object(node, time);
      store = c.e.allocAval(objectAddress, obj, stack, store, c);
      return cont.execute(stack2.addFirst(c.l.abst1(objectAddress)), store, time, c);
      //return objectCont(0).execute(stack, time);
    }
    return c.e.evalNode(properties[0].value, stack.addFirst(objectCont(1)), benv, store, time, c);
  }

jseval.evalHoistedFunctionDeclaration =
  function (node, stack, benva, benv, store, time, c)
  {
    var vr = node.id;
    
    var closure = c.createClosure(node, benva);
    var closureAddress = c.a.closure(node, time);
  
    var prototype = c.createObject(c.OBJECTPA);
    var prototypeObjectAddress = c.a.closureProtoObject(node, time); /*node.body*/
    
    prototype = prototype.add(c.l.userLattice.abst1("constructor"), c.l.abst1(closureAddress));
  
    store = c.e.allocAval(prototypeObjectAddress, prototype, stack, store, c);
  
    closure = closure.add(c.l.U_PROTOTYPE, c.l.abst1(prototypeObjectAddress));
    store = c.e.allocAval(closureAddress, closure, stack, store, c);
    
    var vr = node.id;
    benv = benv.add(c.l.userLattice.abst1(vr.name), c.l.abst1(closureAddress));
  
    return {benv:benv, store: store};
  }

jseval.evalFunctionDeclaration =
  function (node, stack, benva, store, time, c)
  {
    var cont = stack[0];
    var stack2 = stack.slice(1);
    c.e.markNode(node.id);
    node.params.forEach(function (n) { c.e.markNode(n)});
    return cont.execute(stack2.addFirst(c.l.J_UNDEFINED), store, time, c);
  }  

jseval.evalFunctionExpression =
  function (node, stack, benva, store, time, c)
  {
    var cont = stack[0];
    var stack2 = stack.slice(1);
    node.params.forEach(function (n) { c.e.markNode(n)});
  
    var closure = c.createClosure(node, benva);
    var closureAddress = c.a.closure(node, time);
  
    var prototype = c.createObject(c.OBJECTPA);
    var prototypeObjectAddress = c.a.closureProtoObject(node, time); /*node.body*/
    
    prototype = prototype.add(c.l.userLattice.abst1("constructor"), c.l.abst1(closureAddress));
    
    store = c.e.allocAval(prototypeObjectAddress, prototype, stack, store, c);
  
    closure = closure.add(c.l.U_PROTOTYPE, c.l.abst1(prototypeObjectAddress));
  
    store = c.e.allocAval(closureAddress, closure, stack, store, c);
    
    return cont.execute(stack2.addFirst(c.l.abst1(closureAddress)), store, time, c);
  }

jseval.evalNewExpression =
  function (node, stack, benva, store, time, c)
  {
    var calleeNode = node.callee;
    
    function constructorCont()
    {
      var operands = node.arguments;
  
      function operandsCont(i)
      {
        return new Cont("rand", operands[i - 1], null, benva,
          function (stack, store, time, c)
          {
            if (operands.length === i)
            {
              return c.e.applyConstructor(node, stack, benva, store, time, c);
            }
            return c.e.evalNode(operands[i], stack.addFirst(operandsCont(i + 1)), benva, store, time, c);
          });
      }
  
      return new Cont("cons", calleeNode, null, benva,
        function (stack, store, time, c)
        {
          if (operands.length === 0)
          {
            return c.e.applyConstructor(node, stack, benva, store, time, c);
          }
          return c.e.evalNode(operands[0], stack.addFirst(operandsCont(1)), benva, store, time, c);
        });
    }
    
    return c.e.evalNode(calleeNode, stack.addFirst(constructorCont()), benva, store, time, c);
  }

jseval.evalAssignmentExpression =
  function (node, stack, benva, store, time, c)
  { 
    var left = node.left;
    var right = node.right;
    
    c.e.markNode(left);
    switch (left.type)
    {
      case "Identifier":
      {
        function varAssignmentCont()
        {
          return new Cont("=id", right, null, benva,
            function (stack, store, time, c)
            {
              var rvalues = stack[0];
              var cont = stack[1];
              var stack2 = stack.slice(2);
              store = c.e.doScopeSet(c.l.userLattice.abst1(left.name), rvalues, stack, benva, store, c);
              return cont.execute(stack2.addFirst(rvalues), store, time, c);
            });
        }
        
        return c.e.evalNode(right, stack.addFirst(varAssignmentCont()), benva, store, time, c);
      }
      case "MemberExpression":
      {
        function rightCont()
        {
          function memberAssignmentCont()
          {
            return new Cont("=mem", right, null, benva,
              function (stack, store, time, c)
              {
                var rvalues = stack[0];
                var propertyName = stack[1];
                var spn = toUserString(propertyName, store);
                var uspn;
                var length;
                if (uspn = c.l.userLattice.isStringArrayIndex(spn)) // TODO wrong! 'is...Index' should return abstract boolean
                {
                  length = c.l.userLattice.add(uspn, c.l.U_1);
                }
                var objectAddresses = stack[2].addresses();
                var cont = stack[3];
                var stack2 = stack.slice(4);
                //print("rvalues", rvalues, "objectAddresses", objectAddresses, "propertyName", spn);
                if (!objectAddresses)
                {
                  throw new Error("cannot determine object addresses for lhs in " + node);
                }
                objectAddresses.forEach(
                  function (objectAddress)
                  {
                    var object = c.e.lookupAval(objectAddress, stack, store, c);
                    assertDefinedNotNull(object.lookup);
                    object = object.add(spn, rvalues);
                    if (length && object.isArray())
                    {
                      var lengthValue = object.lookup(c.l.U_LENGTH).value; // direct (local) lookup without protochain
                      if (c.l.userLattice.isTrue(c.l.userLattice.lt(lengthValue.user, length)))
                      {
                        object = object.add(c.l.U_LENGTH, new JipdaValue(length, []));
                      }
                    }
                    store = c.e.sideEffectAval(objectAddress, object, stack, store, c);
                  });
                return cont.execute(stack2.addFirst(rvalues), store, time, c);
              });
          }
                
          return new Cont("=right", left, null, benva,
            function (stack, store, time, c)
            {           
              return c.e.evalNode(right, stack.addFirst(memberAssignmentCont()), benva, store, time, c);
            });
        }
          
        return c.e.evalBaseExpression(left, stack.addFirst(rightCont()), benva, store, time, c);
      }
      default:
        throw new Error("evalAssignment: cannot handle left hand side " + left); 
    }
  }

jseval.ToString =
  function (node, stack, benva, store, time, c)
  {
    var value = stack[0];
    if (value.addresses().length === 0)
    {
      var cont = stack[1];
      var stack2 = stack.slice(2);
      var stringValue = new JipdaValue(value.user.ToString(), []);
      return cont.execute(stack2.addFirst(stringValue), store, time, c);
    }
    var stack2 = stack.slice(1);
    return c.e.DefaultValueString(value.addresses(), function (value) {return value.ToString()}, node, stack2, benva, store, time, c);    
  }

jseval.ToStringCont =
  function (stack, store, time, c)
  {
    return c.e.ToString(this.node, stack, this.benva, store, time, c);
  }

//9.9
jseval.ToObject =
  function (value, node, stack, store, time, c)
  {
    var prim = value.user;
    var as = value.addresses(); 
    if (prim === BOT)
    {
      return {store:store, addresses:as};      
    }
//      var pUndefined = prim.projectUndefined();
//      if (pUndefined !== BOT)
//      {
//        tasks.push(new Task("ToObject undefined " + node));
//      }
//      var pNull = prim.projectNull();
//      if (pNull !== BOT)
//      {
//        tasks.push(new Task("ToObject null " + node));
//      }      
//      var pBoolean = prim.projectBoolean();
//      if (pBoolean !== BOT)
//      {
//        throw "TODO";
//      }
//      var pNumber = prim.projectNumber();
//      if (pNumber !== BOT)
//      {
//        throw "TODO";
//      }
      var pString = prim.projectString();
      if (pString !== BOT)
      {
        // copied from constructor (TODO? allocString, ...)
        var stringBenv = c.createString(pString); 
        var stringAddress = c.a.string(node, time);
        stringBenv = stringBenv.add(c.l.U_LENGTH, new JipdaValue(pString.length(), []));
        store = c.e.allocAval(stringAddress, stringBenv, stack, store);
        // end copy
        as = as.addUniqueLast(stringAddress);
      }
      return {store:store, addresses:as};      
    }

//jseval.ToObjectCont =
//  function (stack, store, time, c)
//  {
//    return c.e.ToObject(this.node, stack, this.benva, store, time, c);
//  }
//
//jseval.baseToStringCont =
//  function (stack, store, time, c)
//  {
//    var value = stack
//  }

jseval.evalBaseExpression =
  function (node, stack, benva, store, time, c) 
  {
    var object = node.object;
  
    function baseCont()
    {
      return new Cont("base", object, null, benva,
        function (stack, store, time, c)
        {
          var value = stack[0];
          var cont = stack[1];
          var stack2 = stack.slice(2);

          var toObjectResult = c.e.ToObject(value, node, stack, store, time, c);
          var objectAddresses = new JipdaValue(BOT, toObjectResult.addresses);
          store = toObjectResult.store;
          var property = node.property;
          if (node.computed)
          {
            var cont2 = new Cont("ToString", node, null, benva, c.e.ToStringCont);
            return c.e.evalNode(property, stack2.addFirst(objectAddresses).addFirst(cont).addFirst(cont2), benva, store, time, c);
          }
          // jipda value for property name to correspond with computed property's type
          c.e.markNode(property);
          return cont.execute(stack2.addFirst(objectAddresses).addFirst(c.l.abst1(property.name)), store, time, c);
        });
    }
    
//    var cont = new Cont("ToObject-" + node.tag, benva, c.e.ToObjectCont);
//    cont.node = node;
    return c.e.evalNode(object, stack.addFirst(baseCont())/*.addFirst(cont)*/, benva, store, time, c);
  }

jseval.evalThisExpression =
  function (node, stack, benva, store, time, c)
  {
    var cont = stack[0];
    var stack2 = stack.slice(1);
    //print("looking up 'this' in", benva);
//    var as = c.e.doScopeLookup(c.l.U_THIS, stack, benva, store, c);
    var benv = c.e.lookupAval(benva, stack, store, c);
    var ths = benv.lookup(c.l.U_THIS).value;
    return cont.execute(stack2.addFirst(ths), store, time, c);
  }

jseval.operandsCont =
  function (stack, store, time, c)
  {
    var benva = this.benva;
    var node = this.node;
    var i = this.index;
    var operands = node.arguments;
    if (operands.length === i)
    {
      return c.e.applyProc(node, stack, benva, store, time, c); // 'applyProc' not compatible with 'applyConstructor' (other 'operandsCont')
    }
    var cont = new Cont("rand", node, i + 1, benva, c.e.operandsCont);
    return c.e.evalNode(operands[i], stack.addFirst(cont), benva, store, time, c);
  }

jseval.methodOperatorCont =
  function (stack, store, time, c)
  {
    var benva = this.benva;
    var node = this.node;
    var calleeNode = node.callee;
    var operands = node.arguments;
    var objectAddresses = stack[0].addresses();
    assertTrue(Array.isArray(objectAddresses));
    var propertyName = calleeNode.property.name; // TODO: computed TODO 2 shouldn't this use evalBaseExpression?
    c.e.markNode(calleeNode.property);
    var stack2 = stack.slice(1);
    return objectAddresses.flatMap( // 'map' if Tasks are created
      function (objectAddress)
      {
        var stack3 = stack2.addFirst(c.l.abst1(objectAddress)); // "this" (single address)
//        return new Task("apply method " + propertyName + " on " + objectAddress + " for " + node, //stack3,
//          function () // TODO remove this task level? (see DefaultValue impl)
//          {
            var objectAval = c.e.lookupAval(objectAddress, stack, store, c);
            var memberAval = c.e.doProtoLookup(objectAval, c.l.userLattice.abst1(propertyName), stack, store, c);
//            print("objectAddress", objectAddress, "objectAval", objectAval, "propertyName", propertyName, "result", memberAval);
//            if (memberAval === null)
//            {
//              throw new Error("doProtoLookup: no addresses for " + propertyName + " on " + objectAval);
//            }
            var stack4 = stack3.addFirst(memberAval);
            if (operands.length === 0)
            {
              return c.e.applyProc(node, stack4, benva, store, time, c);
            }
            var cont = new Cont("rand", node, 1, benva, c.e.operandsCont);
            return c.e.evalNode(operands[0], stack4.addFirst(cont), benva, store, time, c);                    
//          });
      });
  }


jseval.evalCallExpression =
  function (node, stack, benva, store, time, c)
  {
    var calleeNode = node.callee;
    var operands = node.arguments;
  
    function operatorCont()
    { 
      return new Cont("rator", calleeNode, null, benva,
        function (stack, store, time, c)
        {
          if (operands.length === 0)
          {
            return c.e.applyProc(node, stack, benva, store, time, c);
          }
          var cont = new Cont("rand", node, 1, benva, c.e.operandsCont);
          return c.e.evalNode(operands[0], stack.addFirst(cont), benva, store, time, c);
        });
    }
    
    if (isMemberExpression(calleeNode))
    {
      c.e.markNode(calleeNode);
      var cont = new Cont("meth", node, null, benva, c.e.methodOperatorCont);
      return c.e.evalNode(calleeNode.object, stack.addFirst(cont), benva, store, time, c);
    }
    
    var stack2 = stack.addFirst(c.GLOBALA);  // global "this" (single address)
    return c.e.evalNode(calleeNode, stack2.addFirst(operatorCont()), benva, store, time, c);
  }

jseval.doReturn = // TODO 'performReturn', like performThrow?
  function (value, stack, store, time, c)
  {
    for (var i = 0; i < stack.length; i++)
    {
      var stackValue = stack[i];
      if (stackValue instanceof Cont)
      {
        if (stackValue.marks.length > 0)
        {
          var stack2 = stack.slice(i + 1);
          return stackValue.execute(stack2.addFirst(value), store, time, c);
        }
      }
    }
    throw new Error("return not in function: " + node);      
  }

jseval.returnCont =
  function (stack, store, time, c)
  {
    var value = stack[0];
    var stack2 = stack.slice(1);
    return c.e.doReturn(value, stack2, store, time, c);
  }
  

jseval.evalReturnStatement =
  function (node, stack, benva, store, time, c)
  {
    if (node.argument === null)
    {
      return c.e.doReturn(c.l.J_UNDEFINED, stack, store, time, c);
    }
  
    var cont = new Cont("ret", node, null, benva, c.e.returnCont); 
    return c.e.evalNode(node.argument, stack.addFirst(cont), benva, store, time, c);
  }

jseval.memberCont =
  function (stack, store, time, c)
  {
    var stringPropertyName = stack[0].user;
    var objectAddresses = stack[1].addresses();
    var cont = stack[2];
    var stack2 = stack.slice(3);
    
    var vals = objectAddresses.map(
      function (objectAddress)
      {
        var objectAval = c.e.lookupAval(objectAddress, stack, store, c);
        var memberAval = c.e.doProtoLookup(objectAval, stringPropertyName, stack, store, c);
//        if (memberAval === null)
//        {
//          throw new Error("doProtoLookup: no addresses for " + stringPropertyName + " on " + objectAval);
//        }
        return memberAval;                      
      });
    var val = vals.reduce(Lattice.join, BOT);
    return cont.execute(stack2.addFirst(val), store, time, c);
  }

jseval.evalMemberExpression =
  function (node, stack, benva, store, time, c)
  {          
    var cont = new Cont("member", node, null, benva, c.e.memberCont);
    return c.e.evalBaseExpression(node, stack.addFirst(cont), benva, store, time, c);
  }

jseval.evalEmptyStatement =
  function (node, stack, benv, store, time, c)
  {
    var cont = stack[0];
    var stack2 = stack.slice(1);
    return cont.execute(stack2.addFirst(c.l.J_UNDEFINED), store, time, c);
  }

jseval.evalIfStatement =
  function (node, stack, benva, store, time, c)
  {
    var testNode = node.test;
    
    function ifCont()
    {
      return new Cont("if", testNode, null, benva,
        function (stack, store, time, c)
        {
          var value = stack[0];
          var booleanValue = toUserBoolean(value);
          var stack2 = stack.slice(1);
          var consequent = node.consequent;
          var alternate = node.alternate;
          if (c.l.userLattice.isFalse(booleanValue))
          {
            if (alternate === null)
            {
              var cont = stack2[0];
              var stack3 = stack2.slice(1);
              return cont.execute(stack3.addFirst(c.l.J_UNDEFINED), store, time, c);
            }
            return c.e.evalNode(alternate, stack2, benva, store, time, c);
          }
          if (c.l.userLattice.isTrue(booleanValue))
          {
            return c.e.evalNode(consequent, stack2, benva, store, time, c);     
          }
          var tasks = [
            new Task("eval consequent of " + testNode.tag, //stack2, 
              function ()
              {
                var time2 = time.tick(consequent.tag, c.k);
                return c.e.evalNode(consequent, stack2, benva, store, time2, c);
              })];
          if (alternate === null)
          {
            tasks = tasks.addLast(
                new Task("eval empty alternate of " + testNode.tag,
                  function ()
                  {
                    var cont = stack2[0];
                    var stack3 = stack2.slice(1);
                    return cont.execute(stack3.addFirst(c.l.J_UNDEFINED), store, time, c);                  
                  }));
          }
          else
          {
            tasks = tasks.addLast(
                new Task("eval non-empty alternate of " + testNode.tag, //stack2, 
                  function ()
                  {
                    var time2 = time.tick(alternate.tag, c.k);
                    return c.e.evalNode(alternate, stack2, benva, store, time2, c);
                  }));
          }
          return tasks;
        });
    }
  
    return c.e.evalNode(testNode, stack.addFirst(ifCont()), benva, store, time, c);
  }
  
jseval.evalArrayExpression =
  function (node, stack, benv, store, time, c)
  {
    var elements = node.elements;
    
    function arrayCont(i)
    {
      return new Cont("array", elements[i - 1], null, benv,
        function (stack, store, time, c)
        {
          if (i === elements.length)
          {
            var exps = stack.slice(0, elements.length).reverse();
            var cont = stack[elements.length];
            var stack2 = stack.slice(elements.length + 1);
            var arr = c.createArray();
            var objectAddress = c.a.array(node, time);
            exps.forEach(
              function (exp, ind)
              {
                var propertyName = c.l.userLattice.abst1(ind).ToString();
                arr = arr.add(propertyName, exp);
              });
            arr = arr.add(c.l.U_LENGTH, c.l.abst1(exps.length));
            store = c.e.allocAval(objectAddress, arr, stack, store, c);
            return cont.execute(stack2.addFirst(c.l.abst1(objectAddress)), store, time, c);
          }
          return c.e.evalNode(elements[i], stack.addFirst(arrayCont(i + 1)), benv, store, time, c);
        });
    }
    
    
    if (elements.length === 0)
    {
      var cont = stack[0];
      var stack2 = stack.slice(1);
      var arr = c.createArray();
      var objectAddress = c.a.array(node, time);
      arr = arr.add(c.l.U_LENGTH, c.l.J_0);
      store = c.e.allocAval(objectAddress, arr, stack, store, c);
      return cont.execute(stack2.addFirst(c.l.abst1(objectAddress)), store, time, c);
    }
    return c.e.evalNode(elements[0], stack.addFirst(arrayCont(1)), benv, store, time, c);
  }

jseval.fortCont =
  function (stack, store, time, c)
  {
    var testAval = stack[0];
    if (c.l.userLattice.isFalse(toUserBoolean(testAval)))
    {
      var bodyAval = stack[1];
      var cont = stack[2];
      var stack2 = stack.slice(3);
      return cont.execute(stack2.addFirst(bodyAval), store, time, c);
    }
    
    var benva = this.benva;
    var node = this.node;
    var body = node.body;

    var time2 = time.tick(node.tag, c.k);
    
    if (c.l.userLattice.isTrue(toUserBoolean(testAval)))
    {
      //discard bodyAval = stack[1]
      var visitedResult = c.v.visited(body, stack, benva, store, time2); 
      if (visitedResult === null)
      {
        return [];
      }
      var store2 = visitedResult.store;
      stack = visitedResult.stack;
      assertDefinedNotNull(stack);
      assertDefinedNotNull(store2);
    
      var stack2 = stack.slice(2);
      var cont = new Cont("forb", node, null, benva, c.e.forbCont);
      return c.e.evalNode(body, stack2.addFirst(cont), benva, store2, time2, c);
//      return new Task("eval body of for-loop " + node.tag, //stack, 
//          function ()
//          {
//            // discard bodyAval = stack[1]
//
//            var store2 = c.v.visited(body, stack, benva, store, time2); 
//            if (store2 === null)
//            {
//              return [];
//            }                                   
////                var store2 = store;
//            
//            var stack2 = stack.slice(2);
//              var cont = new Cont("forb-" + body.tag, benva, c.e.forbCont);
//              cont.node = node;
//            return c.e.evalNode(body, stack2.addFirst(cont), benva, store2, time2, c);
//          });
    }
    var tasks = [
      new Task("exit for-loop " + node.tag, //stack, 
        function ()
        {
          var bodyAval = stack[1];
          var cont = stack[2];
          var stack2 = stack.slice(3);
          return cont.execute(stack2.addFirst(bodyAval), store, time, c); // not time2
        }),
      new Task("eval body of for-loop " + node.tag, //stack, 
        function ()
        {
          // discard bodyAval = stack[1]
          var visitedResult = c.v.visited(body, stack, benva, store, time2); 
          if (visitedResult === null)
          {
            return [];
          }                
          var store2 = visitedResult.store;
          stack = visitedResult.stack;
          assertDefinedNotNull(stack);
          assertDefinedNotNull(store2);

          var stack2 = stack.slice(2);
          var cont = new Cont("forb", node, null, benva, c.e.forbCont);
          return c.e.evalNode(body, stack2.addFirst(cont), benva, store2, time2, c);
        })];
    return tasks;
  }

jseval.foruCont =
  function (stack, store, time, c)
  {
    // discard updateAval = stack[0]
    var stack2 = stack.slice(1);
    var node = this.node;
    var benva = this.benva;
    var test = node.test;
    var cont = new Cont("fort", node, null, benva, c.e.fortCont);
    return c.e.evalNode(test, stack2.addFirst(cont), benva, store, time, c);
  }

jseval.forbCont =
  function (stack, store, time, c)
  {
    var node = this.node;
    var benva = this.benva;
    var update = node.update;
    var cont = new Cont("foru", node, null, benva, c.e.foruCont);
    return c.e.evalNode(update, stack.addFirst(cont), benva, store, time, c);
  }

jseval.foriCont =
  function (stack, store, time, c)
  {
    var node = this.node;
    var benva = this.benva;
    var test = node.test;
    // discard stack[0]: init value
    var stack2 = stack.slice(1);
    var cont = new Cont("fort", node, null, benva, c.e.fortCont);
    // push 'undefined' as the 'result' of unexecuted node.body
    return c.e.evalNode(test, stack2.addFirst(c.l.J_UNDEFINED).addFirst(cont), benva, store, time, c);
  }

jseval.evalForStatement =
  function (node, stack, benva, store, time, c)
  {
    var init = node.init;
    if (init === null)
    {
      var test = node.test;
      var cont = new Cont("fort", node, null, benva, c.e.fortCont);
      // push 'undefined' as the 'result' of unexecuted node.body
      return c.e.evalNode(test, stack.addFirst(c.l.J_UNDEFINED).addFirst(cont), benva, store, time, c);
    }
    var cont = new Cont("fori", node, null, benva, c.e.foriCont);
    return c.e.evalNode(init, stack.addFirst(cont), benva, store, time, c);
  }

jseval.evalUpdateExpression =
  function (node, stack, benva, store, time, c)
  {
    var argument = node.argument;
    c.e.markNode(argument);
    if (isIdentifier(argument))
    {
      var cont = stack[0];
      var stack2 = stack.slice(1);
      var name = c.l.userLattice.abst1(argument.name);
      var value = c.e.doScopeLookup(name, stack, benva, store, c);
      var uold = value.user.ToNumber();
      var jold = new JipdaValue(uold, []);
      var jnew = new JipdaValue((node.operator === "++" ? c.l.userLattice.add(uold, c.l.U_1) : c.l.userLattice.sub(uold, c.l.U_1)), []);
      // TODO doScopeSet has to find the frame again, maybe split doScopeLookup into lookupFrame and lookupFrame+lookupBenv
      store = c.e.doScopeSet(name, jnew, stack, benva, store, c);
      var result = node.prefix ? jnew : jold;
      return cont.execute(stack2.addFirst(result), store, time, c);        
    }
    else if (isMemberExpression(argument))
    {
      function updateMemberCont()
      {
        return new Cont("updMem", argument, null, benva,
          function (stack, store, time, c)
          {
            var propertyName = toUserString(stack[0], store);
            var objectAddresses = stack[1].addresses();
            var cont = stack[2];
            var stack2 = stack.slice(3);
            var result = BOT;
            
            // looking up uses proto chain, setting is local
            objectAddresses.forEach(
              function (objectAddress) 
              {
                var object = c.e.lookupAval(objectAddress, stack, store, c);
                var aval = c.e.doProtoLookup(object, propertyName, stack, store, c);
                if (aval === null)
                {
                  throw new Error("doProtoLookup: no addresses for " + propertyName + " on " + object);
                }
                var uold = toUserNumber(aval, store);
                var jold = new JipdaValue(uold, []);
                var jnew = new JipdaValue((node.operator === "++" ? c.l.userLattice.add(uold, c.l.U_1) : c.l.userLattice.sub(uold, c.l.U_1)), []);
                object = object.add(propertyName, jnew);
                store = c.e.sideEffectAval(objectAddress, object, stack, store, c);
                result = result.join(node.prefix ? jnew : jold);
              });
            return cont.execute(stack2.addFirst(result), store, time, c);
          });
      }
    
      return c.e.evalBaseExpression(argument, stack.addFirst(updateMemberCont()), benva, store, time, c);
    }
    else
    {
      throw new Error("evalUpdateExpression: cannot handle " + argument);
    }
  }

jseval.evalUnaryExpression =
  function (node, stack, benva, store, time, c)
  {
    var argumentNode = node.argument;
    
    function rightCont()
    {
      return new Cont("unr", argumentNode, null, benva,
        function (stack, store, time, c)
        {
          var rightAval = stack[0];
          var cont = stack[1];
          var stack2 = stack.slice(2);
          var robjs = rightAval.as.map(function (a) {return c.e.lookupAval(a, stack, store, c)});
          var result;
          switch (node.operator)
          {
            case "-":
            {
              var robjvals = robjs.map(function (o) {return o.DefaultValue()}).reduce(Lattice.join, BOT);
              var rprim = rightAval.user.join(robjvals);
              result = c.l.userLattice.neg(rprim);
              break;
            }
            case "!":
            {
              var robjvals = robjs.map(function (o) {return o.DefaultValue()}).reduce(Lattice.join, BOT);
              var rprim = rightAval.user.join(robjvals);
              result = c.l.userLattice.not(rprim);
              break;
            }
            case "~":
            {
              var robjvals = robjs.map(function (o) {return o.DefaultValue()}).reduce(Lattice.join, BOT);
              var rprim = rightAval.user.join(robjvals);
              result = c.l.userLattice.binnot(rprim);
              break;
            }
            case "+":
            {
              var robjvals = robjs.map(function (o) {return o.DefaultValue()}).reduce(Lattice.join, BOT);
              var rprim = rightAval.user.join(robjvals);
              result = c.l.userLattice.pos(rprim);
              break;
            }
            default: throw new Error("cannot handle unary operator " + node.operator);
          }
          return cont.execute(stack2.addFirst(new JipdaValue(result, [])), store, time, c);
        });
    }
    
    return c.e.evalNode(argumentNode, stack.addFirst(rightCont()), benva, store, time, c);
  }  

jseval.evalLabeledStatement =
  function (node, stack, benva, store, time, c)
  {
    var cont = stack[0];
    var stack2 = stack.slice(1);
    var handlerCont = cont.setHandler(node);
    return c.e.evalNode(node.body, stack2.addFirst(handlerCont), benva, store, time, c);
  }

jseval.evalBreakStatement =
  function (node, stack, benva, store, time, c)
  {
    var breakValue = c.l.J_UNDEFINED;
    
    // TODO examine whether it is always the case that break value is at stack[1];
    for (var j = 0; j < stack.length; j++)
    {
      var value = stack[j];
      if (value instanceof JipdaValue)
      {
        breakValue = value;
        break;
      }
    }
  //  print("breakValue", breakValue, stack);
    
    if (node.label === null)
    {
      for (var i = 0; i < stack.length; i++)
      {
        var value = stack[i];
        if (value instanceof Cont)
        {
          if (value.handler)
          {
            var handler = value.handler;
            if (isSwitchStatement(handler)) // TODO: labelless breaks in loops
            {
              var stack2 = stack.slice(i);
              return value.execute(stack2.addFirst(breakValue), store, time, c);                              
            }
          }
        }
      }
      throw new Error("no handler for " + node);      
    }
    
    for (var i = 0; i < stack.length; i++)
    {
      var value = stack[i];
      if (value instanceof Cont)
      {
        if (value.handler)
        {
          var handler = value.handler;
          if (isLabeledStatement(handler) && handler.label.name === node.label.name)
          {
            var stack2 = stack.slice(i);
            return value.execute(stack2.addFirst(breakValue), store, time, c);                              
          }
        }
      }
    }    
    throw new Error("no handler for " + node);      
  }
  
jseval.evalSwitchStatement =
  function (node, stack, benva, store, time, c)
  {
    var discriminantNode = node.discriminant;
    
    function switchCont()
    {
      return new Cont("switch", node, null, benva,
        function (stack, store, time, c)
        {
          var discr = stack[0].user;
          
          function execCase(i, stack, store, time, c)
          {
            
            function execCaseCont()
            {
              return new Cont("checkcase", node.cases[i], null, benva,
                  function (stack, store, time, c)
                  {
                    return execCase(i + 1, stack, store, time, c);
                  });
            }
            
            var statements = [];
            for (var j = i; j < node.cases.length; j++)
            {
              statements = statements.concat(node.cases[j].consequent);
            }
            
            var stack2 = stack.slice(1);
            return c.e.evalStatementList(statements, stack2, benva, store, time, c);
          }
          
          function scanCase(i, defaultI, stack, store, time, c)
          {
            function checkCaseCont()
            {
              return new Cont("checkcase", node.cases[i], null, benva,
                function (stack, store, time, c)
                {
                  var selector = stack[0].user;
                  var stack2 = stack.slice(1);
                  if (c.l.userLattice.isTrue(c.l.userLattice.eqq(discr, selector)))
                  {
                    return execCase(i, stack2, store, time, c);
                  }
                  if (c.l.userLattice.isFalse(c.l.userLattice.eqq(discr, selector)))
                  {
                    return scanCase(i + 1, defaultI, stack2, store, time, c);
                  }
                  return [new Task("execute case " + i), function () {return execCase(i, stack2, store, time, c)},
                          new Task("scan case " + i), function() {return scanCase(i + 1, stack2, store, time, c)}];
                });
            }
            
            if (i === node.cases.length)
            {
              if (defaultI === null)
              {
                // var discr = stack[0];
                var cont = stack[1];
                var stack2 = stack.slice(2);
                return cont.execute(stack2.addFirst(c.l.J_UNDEFINED), store, time, c);                              
              }
              
              var statements = [];
              for (var j = defaultI; j < node.cases.length; j++)
              {
                statements = statements.concat(node.cases[j].consequent);
              }
              
              var stack2 = stack.slice(1);
              return c.e.evalStatementList(statements, stack2, benva, store, time, c);
            }
            
            var nodeTest = node.cases[i].test;
            if (nodeTest === null)
            {
              if (i + 1 === node.cases.length)
              {
                return execCase(i, stack, store, time, c);                
              }
              return scanCase(i + 1, i, stack, store, time, c);
            }
            return c.e.evalNode(nodeTest, stack.addFirst(checkCaseCont()), benva, store, time, c);
          }
          
          if (node.cases)
          {
            // push default result value (discr is also on the stack: should not be GCed because this can be object)
            return scanCase(0, null, stack, store, time, c);
          }
          
          var cont = stack[1];
          var stack2 = stack.slice(2);
          return cont.execute(stack2.addFirst(c.l.J_UNDEFINED), store, time, c);
        });
    }
       
    var cont = stack[0];
    var stack2 = stack.slice(1);
    var handlerCont = cont.setHandler(node);
    return c.e.evalNode(discriminantNode, stack2.addFirst(handlerCont).addFirst(switchCont()), benva, store, time, c);
  }

jseval.evalTryStatement =
  function (node, stack, benva, store, time, c)
  {
    var cont = stack[0];
    var stack2 = stack.slice(1);
    var handlerCont = cont.setHandler(node.handlers[0]);
    return c.e.evalNode(node.block, stack2.addFirst(handlerCont), benva, store, time, c);
  }

jseval.evalLogicalExpression =
  function (node, stack, benva, store, time, c)
  {
    // TODO delegate to lattice (as for binary exps) or simply implement logic here?
    // currently: implemented here
    var leftNode = node.left;
    var rightNode = node.right;
    var operator = node.operator;
  
    function leftCont()
    {
      
      function rightCont()
      {
        return new Cont("logr", rightNode, null, benva,
          function (stack, store, time, c)
          {
            var right = stack[0];
            var cont = stack[1];
            var stack2 = stack.slice(2);
            return cont.execute(stack2.addFirst(right), store, time, c);
          });
      }
      
      return new Cont("logl", leftNode, null, benva,
        function (stack, store, time, c)
        {
          var left = stack[0];
          switch (operator)
          {
            case "&&":
              if (c.l.userLattice.isFalse(toUserBoolean(left)))
              {
                var cont1 = stack[1];
                var stack2 = stack.slice(2);
                return cont1.execute(stack2.addFirst(left), store, time, c);
              }
              break;
            case "||":
              if (c.l.userLattice.isTrue(toUserBoolean(left)))
              {
                var cont2 = stack[1];
                var stack3 = stack.slice(2);
                return cont2.execute(stack3.addFirst(left), store, time, c);
              }
              break;
            default: throw new Error("cannot handle logical operator " + operator);
          }
          var stack4 = stack.slice(1);
          return c.e.evalNode(rightNode, stack4.addFirst(rightCont()), benva, store, time, c);
        });
    }
    
    return c.e.evalNode(leftNode, stack.addFirst(leftCont()), benva, store, time, c);
  }

jseval.performThrow =
  function (throwValue, node, stack, benva, store, time, c) // TODO move to top??? calls evalStatementList
  {
    for (var i = 0; i < stack.length; i++)
    {
      var value = stack[i];
      if (value instanceof Cont)
      {
        if (value.handler)
        {
          var handler = value.handler;
          if (isCatchClause(handler))
          {
            var stack2 = stack.slice(i);
            //print("handler", handler, "in cont", value, "for throw value", throwValue);
            var createResult = c.createEnvironment(benva, node, handler, c);
            var extendedBenv = createResult.benv;
            var param = handler.param;
            extendedBenv = extendedBenv.add(c.l.userLattice.abst1(param.name), throwValue);
            var extendedBenva = c.a.benv(handler, time);
            store = c.e.allocAval(extendedBenva, extendedBenv, stack, store, "extended static env for handler with root " + benva);
            // ECMA 12.14:  [...] Return the result of evaluating Catch with parameter B.value.
            // which means we cannot eval catch block as block (which discards last val) ??? REVIEW AFTER evalStatList
            // therefore: eval as sequence
            var block = handler.body;
            return c.e.evalStatementList(block.body, stack2, extendedBenva, store, time, c);                              
          }
        }
      }
    }
    throw new Error(throwValue); // TODO specialize this kind of Error (unhandled exceptions raised by JIPDA)    
  }
  
jseval.evalThrowStatement =
  function (node, stack, benva, store, time, c)
  {
    
    function argumentCont()
    {
      return new Cont("throw", node.argument, null, benva,
        function (stack, store, time, c)
        {
          var throwValue = stack[0];
          var stack2 = stack.slice(1);
          return c.e.performThrow(throwValue, node, stack2, benva, store, time, c);
        });
    }
    
    return c.e.evalNode(node.argument, stack.addFirst(argumentCont()), benva, store, time, c);
  }

jseval.DefaultValue =
  function (objectAddresses, primPostProcessor, node, stack, benva, store, time, c)
  {
    return c.e.DefaultValueNumber(objectAddresses, primPostProcessor, node, stack, benva, store, time, c)
  }
  
jseval.DefaultValueString =
  function (objectAddresses, primPostProcessor, node, stack, benva, store, time, c)
  {
    return c.e.defaultValue("toString", "valueOf", objectAddresses, primPostProcessor, node, stack, benva, store, time, c);
  }
  
jseval.DefaultValueNumber =
  function (objectAddresses, primPostProcessor, node, stack, benva, store, time, c)
  {
    return c.e.defaultValue("valueOf", "toString", objectAddresses, primPostProcessor, node, stack, benva, store, time, c);    
  }
  
  //8.12.8: returns JipdaValue with as = []
jseval.defaultValue =
  function (methodName1, methodName2, objectAddresses, primPostProcessor, node, stack, benva, store, time, c)
  {
    var throwTypeError = (methodName1 === null); 
    var propertyName = c.l.userLattice.abst1(throwTypeError ? methodName2 : methodName1);
    var application = node; // TODO 'synthetic' applications
    return objectAddresses.flatMap( // we do things differently here from regular applyProc (update: still holds?)
        // we create tasks for receiverAddress/Callable pairs (applyProc creates Tasks per receiverA and per Callable
      function (objectAddress)
      {
        var objectAval = c.e.lookupAval(objectAddress, stack, store, c);
  //      print("objectAddress", objectAddress, "objectAval", objectAval);
        var method = c.e.doProtoLookup(objectAval, propertyName, stack, store, c);
        if (method === null)
        {
          throw new Error("TODO");
        }
        var methodFuns = method.as.map(function (a) { return c.e.lookupAval(a, stack, store, c)});
        var allCallable = method.user === BOT && methodFuns.map(function (benv) { return benv.Call.length > 0}).reduce(function (a, b) {return a && b});
        var Callables = methodFuns.flatMap(function (benv) { return benv.Call });
        var cont = defaultValueCont();
        var tasks = Callables.map(
          function (callable)
          {
            var markedCont = callable.mark(cont, application);
            markedCont.toString = cont.toString; // DEBUG
            return new Task("default value " + application, //stack, // orginal stack (not current) for GC purposes
                function ()
                {
                  return callable.applyFunction(application, [], objectAddress, stack.addFirst(markedCont), benva, store, time, c);
                });
          });
        if (!allCallable)
        {
          if (throwTypeError)
          {
            throw new Error("TODO: non-callable second-chance object-to-value coercion must throw type error");
          }
          tasks = tasks.addLast(new Task("not all callable",
            function ()
            {
              // push missing called value
              return c.e.defaultValue(null, methodName2, objectAddresses, primPostProcessor, application, stack.addFirst(BOT), benva, store, time, c);
            }));
        }
        return tasks;
        
        function defaultValueCont()
        {
          return new Cont("defval", node, null, benva,
            function (stack, store, time, c)
            {
              var aval = stack[0];
              
              var cont;
              var stack2;
              if (throwTypeError)
              {
                var aval2 = stack[1]; // called value
                aval = aval.join(aval2);
                cont = stack[2];
                stack2 = stack.slice(3);
                
                if (aval.as.length === 0)
                {
                  return cont.execute(stack2.addFirst(primPostProcessor ? primPostProcessor(aval) : aval), store, time, c);
                }
                
                if (aval.user === BOT)
                {
                  throw new Error("TODO: non-primitive second-chance object-to-value coercion must throw type error");
                }
                
                return [new Task("blah1",
                  function () 
                  {
                    return cont.execute(stack2.addFirst(primPostProcessor ? primPostProcessor(aval) : aval), store, time, c);
                  }),
                  new Task("blah2",
                  function ()
                  {
                    throw new Error("TODO: non-primitive second-chance object-to-value coercion must throw type error");
                  })];
              }
              
              cont = stack[1];
              stack2 = stack.slice(2);                      

              if (aval.as.length === 0)
              {
                return cont.execute(stack2.addFirst(primPostProcessor ? primPostProcessor(aval) : aval), store, time, c);
              }
              
              if (allCallable)
              {
                // all callables during first attempt: no second-chance Task has been created 
                return defaultValue(application, methodName2, objectAddresses, primPostProcessor, application, stack, benva, store, time, c);
              }
              
              // not all callables, but second attempt already launched
              return [];
            });
        }
        
      });
  }

jseval.evalConditionalExpression =
  function (node, stack, benva, store, time, c)
  {
    var testNode = node.test;
    
    function condCont()
    {
      return new Cont("cond", testNode, null, benva,
        function (stack, store, time, c)
        {
          var value = stack[0];
          var booleanValue = toUserBoolean(value);
          var stack2 = stack.slice(1);
          var consequent = node.consequent;
          var alternate = node.alternate;
          if (c.l.userLattice.isFalse(booleanValue))
          {
            return c.e.evalNode(alternate, stack2, benva, store, time, c);
          }
          if (c.l.userLattice.isTrue(booleanValue))
          {
            return c.e.evalNode(consequent, stack2, benva, store, time, c);     
          }
          var tasks = [
            new Task("eval consequent of " + testNode.tag, //stack2, 
              function ()
              {
                var time2 = time.tick(consequent.tag, c.k);
                return c.e.evalNode(consequent, stack2, benva, store, time2, c);
              })];
          tasks = tasks.addLast(
              new Task("eval alternate of " + testNode.tag, //stack2, 
                function ()
                {
                  var time2 = time.tick(alternate.tag, c.k);
                  return c.e.evalNode(alternate, stack2, benva, store, time2, c);
                }));
          return tasks;
        });
    }
  
    return c.e.evalNode(testNode, stack.addFirst(condCont()), benva, store, time, c);
  }

jseval.evalWhileStatement =
  function (node, stack, benva, store, time, c)
  {
    var test = node.test;
    var body = node.body;
  
    function testCont()
    { 
      function bodyCont()
      {
        return new Cont("whileb", body, null, benva,
          function (stack, store, time, c)
          {
            return c.e.evalNode(test, stack.addFirst(testCont()), benva, store, time, c);
          });
      }
    
      return new Cont("whilet", test, null, benva,
        function (stack, store, time, c)
        {
          var testAval = stack[0];
          if (c.l.userLattice.isFalse(toUserBoolean(testAval)))
          {
            var bodyAval = stack[1];
            var cont = stack[2];
            var stack2 = stack.slice(3);
            return cont.execute(stack2.addFirst(bodyAval), store, time, c);
          }
          var time2 = time.tick(node.tag, c.k);
          if (c.l.userLattice.isTrue(toUserBoolean(testAval)))
          {
            // discard bodyAval = stack[1]
            
            var visitedResult = c.v.visited(body, stack, benva, store, time); 
            if (visitedResult === null)
            {
              return [];
            }
            var store2 = visitedResult.store;
            stack = visitedResult.stack;
            assertDefinedNotNull(stack);
            assertDefinedNotNull(store2);

            var stack2 = stack.slice(2);
            return c.e.evalNode(body, stack2.addFirst(bodyCont()), benva, store2, time2, c);
          }
          var tasks = [
            new Task("exit while-loop " + node.tag, //stack, 
              function ()
              {
                var bodyAval = stack[1];
                var cont = stack[2];
                var stack2 = stack.slice(3);
                return cont.execute(stack2.addFirst(bodyAval), store, time2, c);
              }),
            new Task("eval body of while-loop " + node.tag, //stack, 
              function ()
              {
                // discard bodyAval = stack[1]
  
                var visitedResult = c.v.visited(body, stack, benva, store, time2); 
                if (visitedResult === null)
                {
                  return [];
                }
                var store2 = visitedResult.store;
                stack = visitedResult.stack;
                assertDefinedNotNull(stack);
                assertDefinedNotNull(store2);

                var stack2 = stack.slice(2);
                return c.e.evalNode(body, stack2.addFirst(bodyCont()), benva, store2, time2, c);
              })];
          return tasks;
        });
    }
  
    // push 'undefined' as the 'result' of unexecuted node.body
    return c.e.evalNode(test, stack.addFirst(c.l.J_UNDEFINED).addFirst(testCont()), benva, store, time, c);
  }


jseval.markNode =
  function (node)
  {
    node.visited = node.visited ? node.visited + 1 : 1;
  }

jseval.evalNode =
  function (node, stack, benva, store, time, c)
  {
//   print("===== evalNode", "#" + node.tag, node, "\n", stack, benva);
    assertTrue(benva instanceof Addr);
    assertTrue(store instanceof Store);
    assertTrue(!!c);
    c.e.markNode(node);
    switch (node.type)
    {
      case "Literal": 
        return c.e.evalLiteral(node, stack, benva, store, time, c);
      case "Identifier":
        return c.e.evalIdentifier(node, stack, benva, store, time, c);
      case "BinaryExpression":
        return c.e.evalBinaryExpression(node, stack, benva, store, time, c);
      case "LogicalExpression":
        return c.e.evalLogicalExpression(node, stack, benva, store, time, c);
      case "CallExpression":
        return c.e.evalCallExpression(node, stack, benva, store, time, c);
      case "FunctionExpression":
        return c.e.evalFunctionExpression(node, stack, benva, store, time, c);
      case "AssignmentExpression":
        return c.e.evalAssignmentExpression(node, stack, benva, store, time, c);
      case "ArrayExpression":
        return c.e.evalArrayExpression(node, stack, benva, store, time, c);
      case "MemberExpression":
        return c.e.evalMemberExpression(node, stack, benva, store, time, c);
      case "ObjectExpression":
        return c.e.evalObjectExpression(node, stack, benva, store, time, c);
      case "ThisExpression":
        return c.e.evalThisExpression(node, stack, benva, store, time, c);
      case "NewExpression":
        return c.e.evalNewExpression(node, stack, benva, store, time, c);
      case "UpdateExpression":
        return c.e.evalUpdateExpression(node, stack, benva, store, time, c);
      case "UnaryExpression":
        return c.e.evalUnaryExpression(node, stack, benva, store, time, c);
      case "ExpressionStatement":
        return c.e.evalNode(node.expression, stack, benva, store, time, c);
      case "ReturnStatement": 
        return c.e.evalReturnStatement(node, stack, benva, store, time, c);
      case "BreakStatement": 
        return c.e.evalBreakStatement(node, stack, benva, store, time, c);
      case "LabeledStatement": 
        return c.e.evalLabeledStatement(node, stack, benva, store, time, c);
      case "IfStatement": 
        return c.e.evalIfStatement(node, stack, benva, store, time, c);
      case "ConditionalExpression": 
        return c.e.evalConditionalExpression(node, stack, benva, store, time, c);
      case "SwitchStatement": 
        return c.e.evalSwitchStatement(node, stack, benva, store, time, c);
      case "ForStatement": 
        return c.e.evalForStatement(node, stack, benva, store, time, c);
      case "WhileStatement": 
        return c.e.evalWhileStatement(node, stack, benva, store, time, c);
      case "FunctionDeclaration": 
        return c.e.evalFunctionDeclaration(node, stack, benva, store, time, c);
      case "VariableDeclaration": 
        return c.e.evalStatementList(node.declarations, stack, benva, store, time, c);
      case "VariableDeclarator": 
        return c.e.evalVariableDeclarator(node, stack, benva, store, time, c);
      case "BlockStatement":
        return c.e.evalStatementList(node.body, stack, benva, store, time, c);
      case "EmptyStatement":
        return c.e.evalEmptyStatement(node, stack, benva, store, time, c);
      case "TryStatement": 
        return c.e.evalTryStatement(node, stack, benva, store, time, c);
      case "ThrowStatement": 
        return c.e.evalThrowStatement(node, stack, benva, store, time, c);
      case "Program":
        return c.e.evalProgram(node, stack, benva, store, time, c);
      default:
        throw "ipdaEval: cannot handle node " + node.type; 
    }
  }

jseval.applyProc =
  function (application, stack, benva, store, time, c, numberOfOperands)
  {
//    print("applyProc", application);//, "\n", stack, benva, time);
    if (stack.length > 1024)
    {
      throw new Error("stack overflow");
    }
    
    var visitedResult = c.v.visited(application, stack, benva, store, time);
    if (visitedResult === null)
    {
      return [];
    }
    store = visitedResult.store;
    stack = visitedResult.stack;
    
    var applicationLength = (numberOfOperands || application.arguments.length) + 2; // operands + operator + this 
    var applicationValues = stack.slice(0, applicationLength).reverse();
    var ths = applicationValues[0];
    assertTrue(ths.as.length > 0);
    var operatorValues = applicationValues[1].addresses();
    var operandsValues = applicationValues.slice(2);
  //  print("ths", ths, "operator", operatorValues, "operands", operandsValues);
    var stack2 = stack.slice(applicationLength);
    var cont = stack2[0];
    
    if (operatorValues.length === 0)
    {
      return c.e.performThrow(c.l.abst1(applicationValues[1] + " is not a function for " + application.callee), application, stack2, benva, store, time, c);
    }

    var stack3 = stack2.slice(1);
    var time2 = time.tick(application.tag, c.k);

    return ths.addresses().flatMap(
      function (t)
      {
        return operatorValues.flatMap(
            function (operatorValue)
            {
              assertTrue(operatorValue instanceof Addr);
              var functionObject = c.e.lookupAval(operatorValue, stack, store, c);
              var callConc = functionObject.Call;
              assertTrue(callConc.length > 0);
              return callConc.map(
                function (call) 
                {
                  return new Task("#" + application.tag + " " + application + " stack length " + stack.length + " store size " + store.map.entries().length, //stack, // orginal stack (not current) for GC purposes
                      function ()
                      {
                        var markedCont = call.mark(cont, application, operatorValue); 
                        return call.applyFunction(application, operandsValues, t, stack3.addFirst(markedCont), benva, store, time2, c);
                      })
                })
            });
      });
  }

jseval.applyConstructor =
  function (application, stack, benva, store, time, c)
  {
  //  print("applyConstructor", application, "\n", stack, benva, time);
    if (stack.length > 128)
    {
      throw new Error("stack explosion");
    }
    var applicationLength = application.arguments.length + 1;
    var applicationValues = stack.slice(0, applicationLength).reverse();
    var constructorValues = applicationValues[0].addresses();
    var operandsValues = applicationValues.slice(1);
    var stack2 = stack.slice(applicationLength);
    var time2 = time.tick(application.tag, c.k);
    
    return constructorValues.flatMap(
      function (operatorValue)
      {
        var constructor = c.e.lookupAval(operatorValue, stack, store, c);
        // TODO move this closer to applyFunction call, and include declaration node?
        // (so c.e address generators can base themselves on application and declaration node)
        var objectAddress = c.a.constructor(application, time); // was (constructor, time)
    
        function constructorObjectCont()
        {
          return new Cont("consObj", application, null, benva,
            function (stack, store, time, c)
            {
              var objectAval = stack[0];
              var cont = stack[1];
              var stack2 = stack.slice(2);
              if (objectAval.isAddress())
              {
                return cont.execute(stack2.addFirst(objectAval), store, time, c);
              }
              var caddresses = objectAval.addresses();
              return cont.execute(stack2.addFirst(c.l.abst([objectAddress].concat(caddresses))), store, time, c);
            });
        }                    
        
        var cont = constructorObjectCont();
        
        var result = constructor.lookup(c.l.U_PROTOTYPE).value; // seems that we don't require a protochain lookup here (TODO check with ECMA-262 spec)
        // TODO 13.2.2 case when prototype isn't an object 
        var ths = c.createObject(result);
        store = c.e.allocAval(objectAddress, ths, stack, store, c);
        return constructor.Call.map(
            function (call) 
            {
              var markedCont = call.mark(cont, application, operatorValue);
              return new Task("#" + application.tag + " " + application + " stack length " + stack.length + " store size " + store.map.entries().length,//stack, // original stack (not current) for GC purposes
                  function ()
                  {
                    return call.applyFunction(application, operandsValues, objectAddress, stack2.addFirst(markedCont), benva, store, time2, c);
                  })
            })
      });
  }

function BenvClosureCall(node, scope)
{
  this.node = node;
  this.scope = scope;
}

BenvClosureCall.prototype.toString =
  function ()
  {
    return "<BenvClosureCall " + this.node.tag + ">"
  }

BenvClosureCall.prototype.equals =
  function (other)
  {
    if (this === other)
    {
      return true;
    }
    if (!(this instanceof BenvClosureCall))
    {
      return false;
    }
    return this.node === other.node
      && this.scope.equals(other.scope);
  }

BenvClosureCall.prototype.mark =
  function (cont, application, funAddr)
  {
    var markedCont = cont.addMark(new CallMark(application, funAddr, this));
    markedCont.toString = cont.toString; // DEBUG
    return markedCont;
  }

//jseval.annotateDefUse =
//  function (hoisted)
//  {
//    assertDefinedNotNull(hoisted);
//    var du = Ast.defUse(hoisted);
//    du.forEach(
//      function (item)
//      {
//        var node = item.node;
//        if (item.def)
//        {
//          node._def = item.def;
//        }
//        if (item.use)
//        {
//          node._use = item.use;
//        }
//      });
//  }

jseval.applyFunction =
  function (application, funNode, funScope, operandsValues, ths, stack, benva, store, time, c)
  {
    var bodyNodes = funNode.body.body;
    c.e.markNode(funNode.body);
    if (bodyNodes.length === 0)
    {
      var cont = stack[0];
      var stack2 = stack.slice(1);
      return cont.execute(stack2.addFirst(c.l.J_UNDEFINED), store, time, c);
    }
    
    var formalParameters = funNode.params;
  
    var createResult = c.createEnvironment(funScope, application, funNode, c);
    var extendedBenv = createResult.benv;
    
    if (ths === null || ths === undefined)
    {
      extendedBenv = extendedBenv.add(c.l.U_THIS, c.GLOBALA);
    }
    else
    {
      extendedBenv = extendedBenv.add(c.l.U_THIS, c.l.abst1(ths));      
    }
    
    for (var i = 0; i < formalParameters.length; i++)
    {
      var param = formalParameters[i];
      extendedBenv = extendedBenv.add(c.l.userLattice.abst1(param.name), operandsValues[i]);
    }    
    var extendedBenva = c.a.benv(application, time);
    
    var hoisted = funNode._hoisted;
    if (!hoisted)
    {
      var scopeInfo = Ast.scopeInfo(funNode);
      hoisted = Ast.hoist(scopeInfo);
      funNode._hoisted = hoisted;
//      c.e.annotateDefUse(hoisted);
    }
    if (hoisted.funs.length > 0 || hoisted.vars.length > 0)
    {
      hoisted.funs.forEach(
          function (funDecl)
          {
            var result = c.e.evalHoistedFunctionDeclaration(funDecl.node, stack, extendedBenva, extendedBenv, store, time, c);
            extendedBenv = result.benv;
            store = result.store;
          });
      hoisted.vars.forEach(
          function (varDecl)
          {
            var result = c.e.evalHoistedVariableDeclarator(varDecl.node, stack, extendedBenv, store, time, c);
            extendedBenv = result.benv;
            store = result.store;
          });
    }
    
    store = c.e.allocAval(extendedBenva, extendedBenv, stack, store, "extended static env for closure call with root " + funScope);
    
    
    // ECMA 13.2.1: [[Code]] cannot be evaluated as Block,
    // therefore "custom" eval
  
    function fbodyCont(i)
    {
      return new Cont("fbody", bodyNodes[i - 1], null, extendedBenva,
        function (stack, store, time, c)
        {
          if (i === bodyNodes.length)
          {
              // discard aval = stack[0]
            var cont = stack[1];
            var stack2 = stack.slice(2);
            return cont.execute(stack2.addFirst(c.l.J_UNDEFINED), store, time, c);
          }
          var stack3 = stack.slice(1);
          return c.e.evalNode(bodyNodes[i], stack3.addFirst(fbodyCont(i + 1)), extendedBenva, store, time, c);
        });
    }
  
    return c.e.evalNode(bodyNodes[0], stack.addFirst(fbodyCont(1)), extendedBenva, store, time, c);
  }

BenvClosureCall.prototype.applyFunction =
  function (application, operandsValues, ths, stack, benva, store, time, c)
  {
//    print("BenvClosureCall.applyFunction", application, "operandsValues", operandsValues, "ths", ths);

    var funNode = this.node;
    var funScope = this.scope;
    return c.e.applyFunction(application, funNode, funScope, operandsValues, ths, stack, benva, store, time, c);
  }

BenvClosureCall.prototype.addresses =
  function ()
  {
    return [this.scope];
  }
